[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification setlist
enrich
   olist
, 
   oset
with
   

   
   
   functions  list2set : list → set;
              set2list : set → list;
   
   
   
   
   

   

   axioms list2set-empty :  ⊦ list2set([]) = ∅;
          used for: s, ls;
          list2set-rec :  ⊦ list2set(a ' + x) = list2set(x) ++ a;
          used for: s, ls;
          set2list-empty :  ⊦ set2list(∅) = [];
          used for: s, ls;
          set2list-rec :  ⊦ s ≠ ∅ → set2list(s) = s.min + set2list(s.butmin);
          used for: s, ls;

   

   
end enrich